Nuprl Lemma : trivial-component_wf
11,40
postcript
pdf
A
,
B
:Type,
f
:(
A
B
),
ds
:(Id
Type),
da
:(Id
Knd
Type).
trivial-component(
f
)
Component(
ds
;
da
;
A
;
B
)
latex
Definitions
Type
,
t
T
,
x
:
A
B
(
x
)
,
Id
,
Knd
,
x
:
A
.
B
(
x
)
,
Interface(
ds
;
da
;
A
)
,
Top
,
f
(
a
)
,
inl
x
,
x
.
A
(
x
)
,
interface-compose(
f
;
X
)
,
scheme-none()
,
<
a
,
b
>
,
trivial-component(
f
)
,
Component(
ds
;
da
;
A
;
B
)
Lemmas
scheme-none
wf
,
interface-compose
wf
,
top
wf
,
interface
wf
,
Knd
wf
,
Id
wf
origin
A, B:Type, f:(A
B), ds:(IdType), da:(IdKndType).
Component(ds;da;A;B) A, B:Type, f:(AB), ds:(IdType), da:(IdKndType).
Component(ds;da;A;B) TB(x)x:A. B(x)
x.A(x)